(xaL.P(x)) == P(a) & (b:T. a before b  L  P(b)) 

latex

---

clarification:

l_all_since(L;T;a;x.P(x)) == P(a) & (b:T. a before b  L  T  P(b)) 

latex

Definitions	P & Q, x:A. B(x), P  Q, x before y  l
FDL editor aliases	l_all_since